es:ES, x, i:Id, T:Type.
(x, y:T. Dec(x = y  T))
 @i(x:T)
 e'@i.
 (e<e'. (x when e) = (x when e')  T)
  (e:E
  (((e <loc e')
  (c ((((x when e) = (x after e)  T))
  (c & (e'':E. (e <loc e'')  e'' loc e'   ((x when e'') = (x when e')  T))))) 

latex

Definitions	x:A. B(x), P  Q, e@i. P(e), P  Q, x:A. B(x), A c B, (e <loc e'), P & Q, e loc e' , , t  T, x. t(x), e<e'. P(e), T, True, {T}, @i(x:T), P  Q, x(s), P  Q, A, False, Dec(P)
Lemmas	alle-at-iff, alle-lt wf, es-loc wf, es-when wf, es-vartype wf, es-causl wf, not wf, es-loc-pred, es-locl-iff, es-after wf, es-locl wf, es-le-loc, assert wf, es-first wf, es-pred wf, es-dtype wf, decidable wf, Id wf, event system wf, es-le wf, squash wf, true wf, es-E wf, es-pred-locl, es-locl transitivity2, es-le weakening, es-le-iff, es-axioms